(DECLARE (DECIMAL)
	  (SPECIAL AXIOMS CURLIN CURPRF PROOFS SCHEMAS THEOREMS)
	  (SPECIAL LOGICALCONSTANTS QUANTIFIERS)
	  (SPECIAL EXPEXP EXPLGTH EXPLIM ORDCNT)
	  (SPECIAL CONSOLEWIDTH
 		   DDWIDTH
 		   FILEWIDTH
 		   IIIWIDTH
 		   IMLACWIDTH
 		   TTYWIDTH)
	  (SPECIAL *FILEPRINT PRECLIS* *PRINT *TWODIM))


(DEFPROP FIRSTPROP 
 (LAMBDA (L) (CONS (QUOTE CDR) (CDR L))) 
MACRO)

(DEFPROP LASTPROP 
 (LAMBDA (L) (CONS (QUOTE NULL) (CDR L))) 
MACRO)

(DEFPROP NEXTPROP 
 (LAMBDA (L) (CONS (QUOTE CDDR) (CDR L))) 
MACRO)

(DEFPROP PROPNAM 
 (LAMBDA (L) (CONS (QUOTE CAR) (CDR L))) 
MACRO)

(DEFPROP PROPTABLE 
 (LAMBDA (L) (CONS (QUOTE CDR) (CDR L))) 
MACRO)

(DEFPROP PROPVAL 
 (LAMBDA (L) (CONS (QUOTE CADR) (CDR L))) 
MACRO)

(DEFPROP DELETEPROP 
 (LAMBDA(IDENT PROPNAM)
  (PROG (TEM)
	(SETQ TEM IDENT)
   LOOP (COND ((NULL (CDR TEM)) (RETURN NIL)))
	(COND
	 ((EQ (CADR TEM) PROPNAM)
	  (RETURN (PROG2 (RPLACD TEM (CDDDR TEM)) T))))
	(SETQ TEM (CDDR TEM))
	(GO LOOP))) 
EXPR)

(DEFPROP GETGET 
 (LAMBDA(ATOM PROP)
  (PROG (TEM PTAB)
	(SETQ PTAB (FIRSTPROP ATOM))
   LOOP (COND ((LASTPROP PTAB) (RETURN NIL)))
	(SETQ TEM (SEEKPROP (PROPNAM PTAB) PROP))
	(COND ((NOT (NULL TEM)) (RETURN TEM)))
	(SETQ PTAB (NEXTPROP PTAB))
	(GO LOOP))) 
EXPR)

(DEFPROP INITPROP 
 (LAMBDA(IDENT VALUE NAME)
  (RPLACD IDENT (CONS NAME (CONS VALUE (CDR IDENT))))) 
EXPR)

(DEFPROP SEEKPROP 
 (LAMBDA(IDENT PROPNAM)
  (PROG (TEM)
	(SETQ TEM (GETL IDENT (LIST PROPNAM)))
	(COND ((NULL TEM) (RETURN NIL)))
	(RETURN TEM))) 
EXPR)

(DEFPROP AE 
 (LAMBDA(ARGS)
  (PROG (WFF)
	(SETQ WFF (WFFPART (CAR ARGS)))
	(COND
	 ((NOT (EQUAL (CAR WFF) (QUOTE AND)))
	  (ERREND (QUOTE (FIRST ARG IS NOT AN AND)))))
	(ADDLINE (ANDELIM1 WFF (CDR ARGS))
		 (CONS (QUOTE AE) ARGS)
		 (ASSPART (CAR ARGS))))) 
FEXPR)

(DEFPROP AI 
 (LAMBDA(ARGS)
  (ADDLINE (CONJOIN (WFFLIST ARGS))
	   (CONS (QUOTE AI) ARGS)
	   (UNION (ASSLIST ARGS)))) 
FEXPR)

(DEFPROP ALT 
 (LAMBDA(ARGS)
  (PROG (NEWEXP)
	(SETQ NEWEXP
	      (ALT1 (WFFPART (CAR ARGS)) (WFFPART (CADR ARGS))))
	(COND
	 ((NOT (VALID NEWEXP))
	  (ERREND (QUOTE (LINES ARE NOT ALTERNATIVES)))))
	(ADDLINE NEWEXP
		 (LIST (CONS (QUOTE ALT) ARGS))
		 (UNION2 (ASSPART (CAR ARGS))
			 (ASSPART (CADR ARGS)))))) 
FEXPR)

(DEFPROP ASS 
 (LAMBDA(PROP)
  (ADDLINE (CAR PROP) (CONS (QUOTE ASS) PROP) (LIST (NEXTLINE)))) 
FEXPR)

(DEFPROP BS 
 (LAMBDA(ARGS)
  (ADDLINE (BOUNDSUBST (WFFPART (CAR ARGS))
		       (MAKECONSES (CDR ARGS))
 		       NIL)
	   (CONS (QUOTE BS) ARGS)
	   (ASSPART (CAR ARGS)))) 
FEXPR)

(DEFPROP DED 
 (LAMBDA(LINES)
  (PROG NIL
	(COND
	 ((NULL LINES) (ERREND (QUOTE (NOTHING TO CONCLUDE)))))
	(ADDLINE (LIST (QUOTE IMPLIES)
		       (CONJOIN (WFFLIST (CDR LINES)))
		       (WFFPART (CAR LINES)))
		 (CONS (QUOTE DED) LINES)
		 (SETDIF (ASSPART (CAR LINES)) (CDR LINES))))) 
FEXPR)

(DEFPROP DEF 
 (LAMBDA(ARGS)
  (PROG NIL
	(COND
	 ((NOT (ATOM (CAR ARGS)))
	  (ERREND (QUOTE (NAMES MUST BE ATOMS)))))
	(ADDLINE (CONS (QUOTE SETQ) ARGS)
		 (CONS (QUOTE DEF) ARGS)
		 (LIST (NEXTLINE))))) 
FEXPR)

(DEFPROP DNE 
 (LAMBDA(LINE)
  (PROG (NEWSTAT)
	(COND
	 ((NOT
	   (VALID (SETQ NEWSTAT (DOUBLENEG (WFFPART (CAR LINE))))))
	  (ERREND (QUOTE (NO DOUBLE NEGATIVE)))))
	(ADDLINE NEWSTAT
		 (CONS (QUOTE DNE) LINE)
		 (ASSPART (CAR LINE))))) 
FEXPR)

(DEFPROP DNI 
 (LAMBDA(LINE)
  (ADDLINE (LIST (QUOTE NOT)
		 (LIST (QUOTE NOT) (WFFPART (CAR LINE))))
	   (CONS (QUOTE DNI) LINE)
	   (ASSPART (CAR LINE)))) 
FEXPR)

(DEFPROP EG 
 (LAMBDA(ARGS)
  (ADDLINE (EXGEN1 (WFFPART (CAR ARGS)) (CDR ARGS))
	   (CONS (QUOTE EG) ARGS)
	   (ASSPART (CAR ARGS)))) 
FEXPR)

(DEFPROP ELIM 
 (LAMBDA(ARGS)
  (PROG (NEW)
	(SETQ NEW (WFFPART (CADR ARGS)))
	(COND
	 ((NOT (EQUAL (CAR NEW) (QUOTE SETQ)))
	  (ERREND (QUOTE (NO DEFINITION)))))
	(ADDLINE (SUBST (CADDR NEW)
			(CADR NEW)
			(WFFPART (CAR ARGS)))
		 (CONS (QUOTE ELIM) ARGS)
		 (SETDIF (ASSPART (CAR ARGS))
			 (ASSPART (CADR ARGS)))))) 
FEXPR)

(DEFPROP EQE 
 (LAMBDA(ARGS)
  (PROG (NEW)
	(SETQ NEW (WFFPART (CAR ARGS)))
	(COND
	 ((NOT (EQUAL (CAR NEW) (QUOTE EQUIVALENT)))
	  (ERREND (QUOTE (NO EQUIVALENCE)))))
	(SETQ NEW
	      (COND
	       ((EQUAL (CADR ARGS) 2.) (REVERSE (CDR NEW)))
	       (T (CDR NEW))))
	(ADDLINE (CONS (QUOTE IMPLIES) NEW)
		 (CONS (QUOTE EQE) ARGS)
		 (ASSPART (CAR ARGS))))) 
FEXPR)

(DEFPROP EQI 
 (LAMBDA(ARGS)
  (PROG (NEW)
	(COND
	 ((NOT
	   (VALID
	    (SETQ NEW
		  (EQI1 (WFFPART (CAR ARGS))
			(WFFPART (CAR ARGS))))))
	  (ERREND (QUOTE (ARE NOT EQUIVALENT)))))
	(ADDLINE NEW
		 (CONS (QUOTE EQI) ARGS)
		 (UNION2 (ASSPART (CAR ARGS))
			 (ASSPART (CADR ARGS)))))) 
FEXPR)

(DEFPROP ES 
 (LAMBDA(ARGS)
  (ADDLINE (SPECALL (WFFPART (CAR ARGS)) (CDR ARGS))
	   (CONS (QUOTE ES) ARGS)
	   (ASSPART (CAR ARGS)))) 
FEXPR)

(DEFPROP IFE 
 (LAMBDA(ARGS)
  (PROG (NEW)
	(COND
	 ((NOT
	   (VALID
	    (SETQ NEW
		  (IFE1 (WFFPART (CAR ARGS))
			(WFFPART (CADR ARGS))))))
	  (ERREND (QUOTE (NO IF /- THEN /- ELSE EXPRESSION)))))
	(ADDLINE NEW
		 (CONS (QUOTE IFE) ARGS)
		 (UNION2 (ASSPART (CAR ARGS))
			 (ASSPART (CADR ARGS)))))) 
FEXPR)

(DEFPROP IFI 
 (LAMBDA(ARGS)
  (PROG (NEW)
	(COND
	 ((NOT
	   (VALID
	    (SETQ NEW
		  (IFI1 (WFFPART (CAR ARGS))
			(WFFPART (CADR ARGS))))))
	  (ERREND
	   (QUOTE (NEED IMPLICATIONS WITH OPPOSITE ANTECEDENTS)))))
	(ADDLINE NEW
		 (CONS (QUOTE IFI) ARGS)
		 (UNION2 (ASSPART (CAR ARGS))
			 (ASSPART (CADR ARGS)))))) 
FEXPR)

(DEFPROP LC 
 (LAMBDA(ARGS)
  (ADDLINE (LIST (QUOTE EQUAL) ARGS (LAMEXP ARGS))
	   (CONS (QUOTE LC) ARGS)
 	   NIL)) 
FEXPR)

(DEFPROP MP 
 (LAMBDA(ARGS)
  (PROG (NEWSTAT)
	(COND
	 ((NOT
	   (VALID
	    (SETQ NEWSTAT
		  (MP1 (WFFPART (CAR ARGS))
		       (WFFPART (CADR ARGS))))))
	  (ERREND (QUOTE (CANNOT MODUS PONENS)))))
	(ADDLINE NEWSTAT
		 (CONS (QUOTE MP) ARGS)
		 (UNION2 (ASSPART (CAR ARGS))
			 (ASSPART (CADR ARGS)))))) 
FEXPR)

(DEFPROP NE 
 (LAMBDA(ARGS)
  (PROG NIL
	(COND
	 ((NOT
	   (VALID
	    (NOTELIM (WFFPART (CAR ARGS)) (WFFPART (CADR ARGS)))))
	  (ERREND (QUOTE (NO CONTRADICTION)))))
	(ADDLINE (QUOTE FALSE)
		 (CONS (QUOTE NE) ARGS)
		 (UNION2 (ASSPART (CAR ARGS))
			 (ASSPART (CADR ARGS)))))) 
FEXPR)

(DEFPROP NI 
 (LAMBDA(IM)
  (PROG (NEWSTAT)
	(COND
	 ((NOT
	   (VALID (SETQ NEWSTAT (NOTINTRO (WFFPART (CAR IM))))))
	  (ERREND (QUOTE (NO IMPLIES FALSE)))))
	(ADDLINE NEWSTAT (CONS (QUOTE NI) IM) (ASSPART (CAR IM))))) 
FEXPR)

(DEFPROP OE 
 (LAMBDA(ARGS)
  (PROG NIL
	(COND
	 ((OR (NULL ARGS) (NULL (CDR ARGS)))
	  (ERREND (QUOTE (NEED AT LEAST TWO ARGS)))))
	(ADDLINE (ORELIM1 (WFFPART (CAR ARGS))
			  (WFFLIST (CDR ARGS)))
		 (CONS (QUOTE OE) ARGS)
		 (UNION (ASSLIST ARGS))))) 
FEXPR)

(DEFPROP OI 
 (LAMBDA(ARGS)
  (PROG (KNOWN SAVARGS WFFS)
	(SETQ SAVARGS ARGS)
   LOOP (COND
	 ((NULL ARGS)
	  (COND
	   ((NULL KNOWN) (ERREND (QUOTE (NO VALID PROPOSITION))))
	   (T (GO ADDL)))))
	(COND
	 ((NUMBERP (CAR ARGS))
	  (COND ((NULL KNOWN) (SETQ KNOWN (CAR ARGS))))))
	(COND ((NUMBERP (CAR ARGS))
	       (SETQ WFFS (CONS (WFFPART (CAR ARGS)) WFFS)))
	      (T (SETQ WFFS (CONS (CAR ARGS) WFFS))))
	(SETQ ARGS (CDR ARGS))
	(GO LOOP)
   ADDL (ADDLINE (COND ((NULL (CDR WFFS)) (CAR WFFS))
		       (T (CONS (QUOTE OR) (REVERSE WFFS))))
		 (CONS (QUOTE OI) SAVARGS)
		 (ASSPART KNOWN)))) 
FEXPR)

(DEFPROP REP 
 (LAMBDA(ARGS)
  (PROG (NEW)
	(SETQ NEW (WFFPART (CADR ARGS)))
	(COND
	 ((NOT (ISEQUIVALENCE (CAR NEW)))
	  (ERREND (QUOTE (NO EQUATION)))))
	(SETQ NEW
	      (COND
	       ((EQUAL (CADDR ARGS) 2.) (REVERSE (CDR NEW)))
	       (T (CDR NEW))))
	(ADDLINE (SUBST (CADR NEW) (CAR NEW) (WFFPART (CAR ARGS)))
		 (CONS (QUOTE REP) ARGS)
		 (UNION2 (ASSPART (CAR ARGS))
			 (ASSPART (CADR ARGS)))))) 
FEXPR)

(DEFPROP REPL 
 (LAMBDA(ARGS)
  (ADDLINE (REPEITHER (WFFPART (CAR ARGS))
		      (WFFPART (CADR ARGS))
 		      T
		      (CADDR ARGS))
	   (CONS (QUOTE REPL) ARGS)
	   (UNION2 (ASSPART (CAR ARGS)) (ASSPART (CADR ARGS))))) 
FEXPR)

(DEFPROP REPR 
 (LAMBDA(ARGS)
  (ADDLINE (REPEITHER (WFFPART (CAR ARGS))
		      (WFFPART (CADR ARGS))
 		      NIL
		      (CADDR ARGS))
	   (CONS (QUOTE REPR) ARGS)
	   (UNION2 (ASSPART (CAR ARGS)) (ASSPART (CADR ARGS))))) 
FEXPR)

(DEFPROP TAUT 
 (LAMBDA(L)
  (PROG NIL
	(COND
	 ((NOT (TH1 NIL NIL (WFFLIST (CDR L)) (LIST (CAR L))))
	  (ERREND (QUOTE (DOES NOT FOLLOW)))))
	(ADDLINE (CAR L)
		 (CONS (QUOTE TAUT) L)
		 (UNION (ASSLIST (CDR L)))))) 
FEXPR)

(DEFPROP UG 
 (LAMBDA(ARGS)
  (PROG (ASS VARS WFF)
	(SETQ WFF (WFFPART (CAR ARGS)))
	(SETQ ASS (ASSPART (CAR ARGS)))
	(SETQ VARS (CDR ARGS))
   LOOP (COND ((NULL VARS) (GO ADDL)))
	(COND ((ATOM (CAR VARS)) (GO ATOM)))
	(COND ((EQUAL (CAAR VARS) (QUOTE CONS)) (GO DOT)))
	(ERREND (QUOTE (ILLEGAL ARGUMENT)))
   ATOM (SETQ WFF (UNGEN WFF ASS (CAR VARS) (CAR VARS)))
	(GO ELOOP)
   DOT  (SETQ WFF (UNGEN WFF ASS (CADAR VARS) (CADDAR VARS)))
   ELOOP
	(SETQ VARS (CDR VARS))
	(GO LOOP)
   ADDL (ADDLINE WFF (CONS (QUOTE UG) ARGS) (ASSPART (CAR ARGS))))) 
FEXPR)

(DEFPROP US 
 (LAMBDA(ARGS)
  (PROG NIL
	(ADDLINE (SPECALL (WFFPART (CAR ARGS)) (CDR ARGS))
		 (CONS (QUOTE US) ARGS)
		 (ASSPART (CAR ARGS))))) 
FEXPR)

(DEFPROP USEAX 
 (LAMBDA(ARGS)
  (PROG (AX FORM)
	(SETQ AX (GET (CAR ARGS) (QUOTE AXIOM)))
	(COND ((NULL AX) (ERREND (QUOTE (NO SUCH AXIOM)))))
	(SETQ FORM (SPECALL AX (CDR ARGS)))
	(ADDLINE FORM (CONS (QUOTE USEAX) ARGS) NIL))) 
FEXPR)

(DEFPROP USESCHM 
 (LAMBDA(ARGS)
  (PROG (SCHEMA)
	(SETQ SCHEMA (GET (CAR ARGS) (QUOTE SCHEMA)))
	(COND ((NULL SCHEMA) (ERREND (QUOTE (IS NOT SCHEMA)))))
	(ADDLINE (LAMEXP
		  (PROPSUBST (CADR ARGS)
			     (CADAR SCHEMA)
			     (CADR SCHEMA)))
		 (CONS (QUOTE USESCHM) ARGS)
 		 NIL))) 
FEXPR)

(DEFPROP USETHM 
 (LAMBDA(ARGS)
  (PROG (TH FORM)
	(SETQ TH (GET (CAR ARGS) (QUOTE THEOREM)))
	(COND ((NULL TH) (ERREND (QUOTE (NO SUCH THEOREM)))))
	(SETQ FORM (SPECALL TH (CDR ARGS)))
	(ADDLINE FORM (CONS (QUOTE USETHM) ARGS) NIL))) 
FEXPR)

(DEFPROP BT 
 (LAMBDA(LINO)
  (PROG (PROOF)
	(SETQ LINO
	      (COND
	       ((NULL LINO) (DIFFERENCE (CURLINE) 1.))
	       (T (CAR LINO))))
	(SETQ PROOF (CURTEXT))
	(COND
	 ((OR (GREATERP LINO (CURLINE)) (LESSP LINO 0.))
	  (ERREND (QUOTE (NON EXISTANT LINE)))))
	(COND ((EQUAL LINO 0.)
	       (PUTPROP (CURPROOF) NIL (QUOTE PROOF)))
	      (T
	       (PROG NIL
		     (RPLACD (NTHCDR PROOF (DIFFERENCE LINO 1.))
 			     NIL)
		     (PUTPROP (CURPROOF) PROOF (QUOTE PROOF)))))
	(INITPROOF (CURPROOF))
	(SHOWCURLINE))) 
FEXPR)

(DEFPROP FINDL 
 (LAMBDA(L)
  (PROG (PRF TXT WFF)
	(SETQ WFF (CAR L))
	(SETQ PRF
	      (COND ((NOT (NULL (CDR L))) (CADR L))
		    (T (CURPROOF))))
	(SETQ TXT (GET PRF (QUOTE PROOF)))
   LOOP (COND ((NULL TXT) (RETURN NIL)))
	(COND ((EQUAL WFF (CADAR TXT)) (SHOWLINE (CAR TXT))))
	(SETQ TXT (CDR TXT))
	(GO LOOP))) 
FEXPR)

(DEFPROP GIVEAX 
 (LAMBDA(L)
  (PROG NIL
	(COND
	 ((NOT (ATOM (CAR L)))
	  (ERREND (QUOTE (NON ATOMIC AXIOM NAME)))))
	(COND
	 ((NOT (MEMBER (CAR L) AXIOMS))
	  (SETQ AXIOMS (APPEND AXIOMS (LIST (CAR L))))))
	(PUTPROP (CAR L) (CADR L) (QUOTE AXIOM))
	(COND (*PRINT (SHOWAXIOM (CAR L)))))) 
FEXPR)

(DEFPROP GIVESCHM 
 (LAMBDA(L)
  (PROG NIL
	(COND
	 ((NOT (ATOM (CAR L)))
	  (ERREND (QUOTE (NON ATOMIC SCHEMA NAME)))))
	(COND
	 ((NOT (MEMBER (CAR L) SCHEMAS))
	  (SETQ SCHEMAS (APPEND SCHEMAS (LIST (CAR L))))))
	(PUTPROP (CAR L) (CADR L) (QUOTE SCHEMA))
	(COND (*PRINT (SHOWSCHEMA (CAR L)))))) 
FEXPR)

(DEFPROP INVENTORY 
 (LAMBDA NIL
  (PROG NIL
	(COND
	 ((NOT (NULL AXIOMS))
	  (PROG NIL
		(TERPRI)
		(PRINT (QUOTE AXIOMS))
		(PRINL AXIOMS))))
	(COND
	 ((NOT (NULL SCHEMAS))
	  (PROG NIL
		(TERPRI)
		(PRINT (QUOTE SCHEMAS))
		(PRINL SCHEMAS))))
	(COND
	 ((NOT (NULL PROOFS))
	  (PROG NIL
		(TERPRI)
		(PRINT (QUOTE PROOFS))
		(PRINL PROOFS))))
	(COND
	 ((NOT (NULL THEOREMS))
	  (PROG NIL
		(TERPRI)
		(PRINT (QUOTE THEOREMS))
		(PRINL THEOREMS)))))) 
EXPR)

(DEFPROP MAKETHM 
 (LAMBDA(ARG)
  (MAKETHEOREM1 (CAR ARG)
		(CADR ARG)
		(COND
		 ((NOT (NULL (CDDR ARG))) (CADDR ARG))
		 (T (CURPROOF))))) 
FEXPR)

(DEFPROP ONDD 
 (LAMBDA NIL
  (PROG NIL
	(INITSTANCHARSET)
	(LINELENGTH (SETQ CONSOLEWIDTH DDWIDTH)))) 
EXPR)

(DEFPROP ONIII 
 (LAMBDA NIL
  (PROG NIL
	(INITSTANCHARSET)
	(LINELENGTH (SETQ CONSOLEWIDTH IIIWIDTH)))) 
EXPR)

(DEFPROP ONIMLAC 
 (LAMBDA NIL
  (PROG NIL
	(INITSTANCHARSET)
	(LINELENGTH (SETQ CONSOLEWIDTH IMLACWIDTH)))) 
EXPR)

(DEFPROP ONTTY 
 (LAMBDA NIL
  (PROG NIL
	(INITTTYCHARSET)
	(LINELENGTH (SETQ CONSOLEWIDTH TTYWIDTH)))) 
EXPR)

(DEFPROP PROOF 
 (LAMBDA(NAME)
  (PROG NIL
	(COND ((NULL NAME) (ERREND (QUOTE (NO NAME GIVEN)))))
	(COND
	 ((NOT (ATOM (CAR NAME)))
	  (ERREND (QUOTE (NON ATOMIC PROOF NAME)))))
	(INITPROOF (CAR NAME))
	(COND (*PRINT (SHOWCURLINE))))) 
FEXPR)

(DEFPROP REDO 
 (LAMBDA(ARGS)
  (PROG (CHANGED CURL LASTL NEWC)
	(COND
	 ((NOT (EQUAL (WFFPART (CAR ARGS)) (WFFPART (CADR ARGS))))
	  (ERREND (QUOTE (CANNOT REDO)))))
	(SETQ CHANGED (CONS (CONS (CAR ARGS) (CADR ARGS)) NIL))
	(SETQ CURL (PLUS (CAR ARGS) 1.))
	(SETQ LASTL (PLUS (CURLINE) 1.))
   LOOP (COND ((EQ CURL LASTL) (RETURN NIL)))
	(SETQ NEWC (SUBLIS CHANGED (BYPART CURL)))
	(COND ((EQUAL NEWC (BYPART CURL)) (GO ELOOP))
	      (T (EVAL NEWC)))
	(SETQ CHANGED (CONS (CONS CURL (CURLINE)) CHANGED))
   ELOOP
	(SETQ CURL (PLUS CURL 1.))
	(GO LOOP))) 
FEXPR)

(DEFPROP RESTOREALL 
 (LAMBDA(FILES)
  (PROG (DEV FILE *PRINT)
	(COND (*FILEPRINT (PROG NIL (SETQ *PRINT T))))
	(SETQ DEV (QUOTE DSK:))
   LOOP (COND ((NULL FILES) (GO EXIT)))
	(SETQ FILE (CAR FILES))
	(COND ((ATOM FILE) (GO READ)))
	(COND ((EQUAL (CAR FILE) (QUOTE QUOTE)) (GO DEVICE)))
	(COND ((EQUAL (CAR FILE) (QUOTE CONS)) (GO DOTTED)))
	(ERREND (QUOTE (NOT FILE OR DEVICE NAME)))
   READ (READIN DEV (LIST FILE) NIL)
	(GO ELOOP)
   DOTTED
	(SETQ FILE (CONS (CADR FILE) (CADDR FILE)))
	(GO READ)
   DEVICE
	(SETQ DEV (CADR FILE))
	(GO ELOOP)
   ELOOP
	(SETQ FILES (CDR FILES))
	(GO LOOP)
   EXIT (INVENTORY))) 
FEXPR)

(DEFPROP SAVEALL 
 (LAMBDA(FILE)
  (PROG (DEV ITEM)
	(SETQ DEV (QUOTE DSK:))
   LOOP (COND ((NULL FILE) (ERREND (QUOTE (DEVICE BUT NO FILE)))))
	(SETQ ITEM (CAR FILE))
	(COND ((ATOM ITEM) (GO OUTPUT)))
	(COND ((EQUAL (CAR ITEM) (QUOTE QUOTE)) (GO DEVICE)))
	(COND ((EQUAL (CAR ITEM) (QUOTE CONS)) (GO DOTTED)))
	(ERREND (QUOTE (NOT FILE SPECIFIER)))
   DEVICE
	(SETQ DEV (CADR ITEM))
	(SETQ FILE (CDR FILE))
	(GO LOOP)
   DOTTED
	(SETQ ITEM (CONS (CADR ITEM) (CADDR ITEM)))
   OUTPUT
	(EVAL (LIST (QUOTE OUTPUT) DEV ITEM))
	(OUTC T NIL)
	(LINELENGTH FILEWIDTH)
	(MAPC (FUNCTION SAVEAXIOM) AXIOMS)
	(MAPC (FUNCTION SAVESCHEMA) SCHEMAS)
	(MAPC (FUNCTION SAVEPROOF) PROOFS)
	(MAPC (FUNCTION SAVETHEOREM) THEOREMS)
	(OUTC NIL T)
	(INVENTORY))) 
FEXPR)

(DEFPROP SAVECOMS 
 (LAMBDA(FILE)
  (PROG (DEV ITEM)
	(SETQ DEV (QUOTE DSK:))
   LOOP (COND ((NULL FILE) (ERREND (QUOTE (NO FILE SPECIFIED)))))
	(SETQ ITEM (CAR FILE))
	(COND ((ATOM ITEM) (GO OUTPUT)))
	(COND ((EQUAL (CAR ITEM) (QUOTE QUOTE)) (GO DEVICE)))
	(COND ((EQUAL (CAR ITEM) (QUOTE CONS)) (GO DOTTED)))
	(ERREND (QUOTE (NOT FILE SPECIFIER)))
   DEVICE
	(SETQ DEV (CADR ITEM))
	(SETQ FILE (CDR FILE))
	(GO LOOP)
   DOTTED
	(SETQ ITEM (CONS (CADR ITEM) (CADDR ITEM)))
   OUTPUT
	(EVAL (LIST (QUOTE OUTPUT) DEV ITEM))
	(OUTC T NIL)
	(LINELENGTH FILEWIDTH)
	(MAPC (FUNCTION SAVEAXCOM) AXIOMS)
	(MAPC (FUNCTION SAVESCHMCOM) SCHEMAS)
	(MAPC (FUNCTION SAVEPRFCOM) PROOFS)
	(MAPC (FUNCTION SAVETHMCOM) THEOREMS)
	(OUTC NIL T)
	(INVENTORY))) 
FEXPR)

(DEFPROP SHOW 
 (LAMBDA(THINGS)
  (PROG (LINE1 LINE2 TEM)
   TOP  (COND ((NULL THINGS) (RETURN (SHOWPROOF (CURPROOF)))))
   LOOP (COND ((NULL THINGS) (GO EXIT)))
	(COND ((NOT (ATOM (CAR THINGS))) (GO DEV)))
	(COND ((NUMBERP (CAR THINGS)) (GO LINES)))
	(SETQ TEM (GETGET (CAR THINGS) (QUOTE IMAGE)))
	(COND ((NULL TEM) (ERREND (QUOTE (NOTHING TO SHOW)))))
	((CADR TEM) (CAR THINGS))
   ELOOP
	(SETQ THINGS (CDR THINGS))
	(GO LOOP)
   LINES
	(SETQ LINE1 (CAR THINGS))
	(SETQ THINGS (CDR THINGS))
	(COND
	 ((OR (NULL THINGS) (NOT (NUMBERP (CAR THINGS))))
	  (SETQ LINE2 LINE1))
	 (T
	  (PROG NIL
		(SETQ LINE2 (CAR THINGS))
		(SETQ THINGS (CDR THINGS)))))
   LLOOP
	(COND ((GREATERP LINE1 LINE2) (GO EXIT)))
	(SHOWLINE (GETLINE LINE1))
	(SETQ LINE1 (PLUS LINE1 1.))
	(GO LLOOP)
   DEV  (COND
	 ((NOT (EQUAL (CAAR THINGS) (QUOTE QUOTE)))
	  (ERREND (QUOTE (NEED NAME OR FILE SPEC)))))
	(EVAL (CONS (QUOTE OUTPUT) (CADAR THINGS)))
	(OUTC T T)
	(SETQ THINGS (CDR THINGS))
	(GO TOP)
   EXIT (OUTC NIL T))) 
FEXPR)

(DEFPROP SHOWALL 
 (LAMBDA(FILE)
  (PROG (DEV ITEM)
	(SETQ DEV (QUOTE DSK:))
   LOOP (COND ((NULL FILE) (ERREND (QUOTE (NO FILE SPECIFIED)))))
	(SETQ ITEM (CAR FILE))
	(COND ((ATOM ITEM) (GO OUTPUT)))
	(COND ((EQUAL (CAR ITEM) (QUOTE QUOTE)) (GO DEVICE)))
	(COND ((EQUAL (CAR ITEM) (QUOTE CONS)) (GO DOTTED)))
	(ERREND (QUOTE (NOT FILE SPECIFIER)))
   DEVICE
	(SETQ DEV (CADR ITEM))
	(SETQ FILE (CDR FILE))
	(GO LOOP)
   DOTTED
	(SETQ ITEM (CONS (CADR ITEM) (CADDR ITEM)))
   OUTPUT
	(EVAL (LIST (QUOTE OUTPUT) DEV ITEM))
	(OUTC T NIL)
	(LINELENGTH FILEWIDTH)
	(MAPC (FUNCTION SHOWAXIOM) AXIOMS)
	(MAPC (FUNCTION SHOWSCHEMA) SCHEMAS)
	(MAPC (FUNCTION SHOWPROOF) PROOFS)
	(MAPC (FUNCTION SHOWTHEOREM) THEOREMS)
	(OUTC NIL T)
	(INVENTORY))) 
FEXPR)

(DEFPROP SSEX 
 (LAMBDA(L)
  (PROG (LINE NAME PRF)
	(SETQ NAME (COND ((NULL L) (CURPROOF)) (T (CAR L))))
	(SETQ PRF (GETL NAME (QUOTE (PROOF))))
	(COND
	 ((NULL PRF) (ERREND (QUOTE (NO PROOF BY THAT NAME)))))
	(SETQ PRF (CADR PRF))
	(PRINT (QUOTE PROOF))
	(PRINS NAME)
   LOOP (COND ((NULL PRF) (RETURN NIL)))
	(SETQ LINE (CAR PRF))
	(TERPRI)
	(PRINC (CAR LINE))
	(PRINC (QUOTE //))
	(PRINTSUBEXPR (CADR LINE) (CURCOL) 0.)
	(COND
	 ((GREATERP (PLUS (FLATSIZE (CDDR LINE)) 6.) (CHRCT))
	  (GO MANY)))
	(PRINC (QUOTE //))
	(PRINS (QUOTE BY))
	(PRINS (CADDR LINE))
	(COND
	 ((NOT (NULL (CADDDR LINE)))
	  (PROG NIL (PRINS (QUOTE ASS)) (PRIN1 (CADDDR LINE)))))
   ELOOP
	(SETQ PRF (CDR PRF))
	(GO LOOP)
   MANY (TERPRI)
	(PRINTN (QUOTE //) 4.)
	(PRINC (QUOTE BY))
	(PRINC (QUOTE //))
	(PRINTSUBEXPR (CADDR LINE) (CURCOL) 0.)
	(COND ((NULL (CADDDR LINE)) (GO ELOOP)))
	(TERPRI)
	(PRINTN (QUOTE //) 4.)
	(PRINC (QUOTE ASS))
	(PRINC (QUOTE //))
	(PRINS (CADDDR LINE))
	(GO ELOOP))) 
FEXPR)

(DEFPROP ADDLINE 
 (LAMBDA(WFF JUST ASS)
  (PROG NIL
	(PUTPROP (CURPROOF)
		 (NCONC (CURTEXT)
			(LIST
			 (LIST (PLUS (CURLINE) 1.) WFF JUST ASS)))
		 (QUOTE PROOF))
	(SETQ CURLIN (PLUS CURLIN 1.))
	(PUTPROP (QUOTE /@) (CURLINE) (QUOTE NEWNAM))
	(COND (*PRINT (SHOWCURLINE))))) 
EXPR)

(DEFPROP ADDAXIOM 
 (LAmBDA(L)
  (PROG NIL
	(PUTPROP (CAR L) (CADR L) (QUOTE AXIOM))
	(SETQ AXIOMS (CONS (CAR L) AXIOMS)))) 
FEXPR)

(DEFPROP ADDSCHEMA 
 (LAMBDA(L)
  (PROG NIL
	(PUTPROP (CAR L) (CADR L) (QUOTE SCHEMA))
	(SETQ SCHEMAS (CONS (CAR L) SCHEMAS)))) 
FEXPR)

(DEFPROP ADDTHEOREM 
 (LAMBDA(L)
  (PROG NIL
	(PUTPROP (CAR L) (CADR L) (QUOTE THEOREM))
	(SETQ THEOREMS (CONS (CAR L) THEOREMS)))) 
FEXPR)

(DEFPROP ALPHAPART 
 (LAMBDA(IDENT)
  (PROG (CHARS)
	(SETQ CHARS (REVERSE (EXPLODE IDENT)))
   LOOP (COND
	 ((NOT (NUMBERP (CAR CHARS)))
	  (RETURN (READLIST (REVERSE CHARS)))))
	(SETQ CHARS (CDR CHARS))
	(GO LOOP))) 
EXPR)

(DEFPROP ALLVARS 
 (LAMBDA (EXPRESSION) (ALLVARS1 EXPRESSION NIL)) 
EXPR)

(DEFPROP ALLVARS1 
 (LAMBDA(EXP VARS)
  (COND
   ((ATOM EXP)
    (COND
     ((ISVAR EXP)
      (COND ((MEMBER EXP VARS) VARS) (T (CONS EXP VARS))))
     (T VARS)))
   (T (ALLVARSL (CDR EXP) VARS)))) 
EXPR)

(DEFPROP ALLVARSL 
 (LAMBDA(EXPL VARS)
  (COND ((NULL EXPL) VARS)
	(T (ALLVARS1 (CAR EXPL) (ALLVARSL (CDR EXPL) VARS))))) 
EXPR)

(DEFPROP ALT1 
 (LAMBDA(I1 I2)
  ((LAMBDA(U V)
    (COND ((VALID U) (SUBLIS U (QUOTE QQQ)))
	  ((VALID V) (SUBLIS V (QUOTE QQQ)))
	  (T (QUOTE INVALID))))
   (INST (CONS I1 I2)
	 (QUOTE ((IMPLIES PPP QQQ) IMPLIES (NOT PPP) QQQ))
 	 NIL)
   (INST (CONS I2 I1)
	 (QUOTE ((IMPLIES PPP QQQ) IMPLIES (NOT PPP) QQQ))
 	 NIL))) 
EXPR)

(DEFPROP ANDELIM1 
 (LAMBDA(WFF PLACES)
  (PROG (CHOSEN LEN)
	(SETQ LEN (LENGTH (CDR WFF)))
	(COND
	 ((NEQ (CAR WFF) (QUOTE AND))
	  (ERREND (QUOTE (FIRST ARG IS NOT AN AND)))))
   LOOP (COND ((NULL PLACES) (RETURN (CONJOIN (REVERSE CHOSEN)))))
	(COND
	 ((GREATERP (CAR PLACES) LEN)
	  (ERREND (QUOTE (TOO FEW CONJUNCTS)))))
	(SETQ CHOSEN (CONS (NTHELT (CDR WFF) (CAR PLACES)) CHOSEN))
	(SETQ PLACES (CDR PLACES))
	(GO LOOP))) 
EXPR)

(DEFPROP ASSLIST 
 (LAMBDA (L) (MAPCAR (FUNCTION ASSPART) L)) 
EXPR)

(DEFPROP ASSOCR 
 (LAMBDA(ITM LST)
  (PROG NIL
   LOOP (COND ((NULL LST) (RETURN NIL)))
	(COND ((EQ ITM (CDAR LST)) (RETURN (CAR LST))))
	(SETQ LST (CDR LST))
	(GO LOOP))) 
EXPR)

(DEFPROP ASSPART 
 (LAMBDA (LINE) (CADDDR (GETLINE LINE))) 
EXPR)

(DEFPROP BINAND 
 (LAMBDA(ARGS)
  (COND ((NULL ARGS) (QUOTE (AND TRUE TRUE)))
	((NULL (CDR ARGS))
	 (LIST (QUOTE AND) (CAR ARGS) (QUOTE TRUE)))
	((NULL (CDDR ARGS)) (CONS (QUOTE AND) ARGS))
	(T (LIST (QUOTE AND) (CAR ARGS) (BINAND (CDR ARGS)))))) 
EXPR)

(DEFPROP BINOR 
 (LAMBDA(ARGS)
  (COND ((NULL ARGS) (QUOTE (OR FALSE FALSE)))
	((NULL (CDR ARGS))
	 (LIST (QUOTE OR) (CAR ARGS) (QUOTE FALSE)))
	((NULL (CDDR ARGS)) (CONS (QUOTE OR) ARGS))
	(T (LIST (QUOTE OR) (CAR ARGS) (BINOR (CDR ARGS)))))) 
EXPR)

(DEFPROP BYPART 
 (LAMBDA (LINE) (CADDR (GETLINE LINE))) 
EXPR)

(DEFPROP BOUNDSUBST 
 (LAMBDA(EXP SUBS BINDS)
  (PROG (TEM)
	(COND ((ATOM EXP) (GO ATOM)))
	(COND ((ISQUANT (CAAR EXP)) (GO QUANT)))
	(RETURN (BOUNDSUBSTL EXP SUBS BINDS))
   ATOM (COND ((ISCONST EXP) (RETURN EXP)))
	(SETQ TEM (ASSOC EXP BINDS))
	(COND ((NOT (NULL TEM)) (RETURN (CDR TEM))))
	(SETQ TEM (ASSOCR EXP BINDS))
	(COND
	 ((NOT (NULL TEM))
	  (ERREND (QUOTE (FREE VARIABLE CAPTURE)))))
	(RETURN EXP)
   QUANT
	(SETQ TEM (ASSOC (CADAR EXP) SUBS))
	(SETQ TEM
	      (COND ((NOT (NULL TEM)) (CDR TEM)) (T (CADAR EXP))))
	(COND
	 ((NOT (NULL (ASSOCR TEM BINDS)))
	  (ERREND (QUOTE (BOUND VARIABLE CAPTURE)))))
	(RETURN
	 (LIST (LIST (CAAR EXP) TEM)
	       (BOUNDSUBST (CADR EXP)
 			   SUBS
			   (CONS (CONS (CADAR EXP) TEM) BINDS)))))) 
EXPR)

(DEFPROP BOUNDSUBSTL 
 (LAMBDA(LST SUBS BINDS)
  (COND ((NULL LST) NIL)
	(T
	 (CONS (BOUNDSUBST (CAR LST) SUBS BINDS)
	       (BOUNDSUBSTL (CDR LST) SUBS BINDS))))) 
EXPR)

(DEFPROP CONJOIN 
 (LAMBDA(WFFS)
  (COND ((NULL WFFS) (QUOTE TRUE))
	((NULL (CDR WFFS)) (CAR WFFS))
	(T (CONS (QUOTE AND) WFFS)))) 
EXPR)

(DEFPROP CURCOL 
 (LAMBDA NIL (PLUS (LINELENGTH NIL) (DIFFERENCE 1. (CHRCT)))) 
EXPR)

(DEFPROP CURLINE 
 (LAMBDA NIL (PROG2 (CURPROOF) CURLIN)) 
EXPR)

(DEFPROP CURPROOF 
 (LAMBDA NIL
  (COND ((NULL CURPRF) (ERREND (QUOTE (NO CURRENT PROOF))))
	(T CURPRF))) 
EXPR)

(DEFPROP CURTEXT 
 (LAMBDA NIL (GET (CURPROOF) (QUOTE PROOF))) 
EXPR)

(DEFPROP DOUBLENEG 
 (LAMBDA(PROP)
  ((LAMBDA(W)
    (COND ((NOT (VALID W)) (QUOTE INVALID))
	  (T (SUBLIS W (QUOTE PPP)))))
   (INST PROP (QUOTE (NOT (NOT PPP))) NIL))) 
EXPR)

(DEFPROP EXGEN1 
 (LAMBDA(WFF VARS)
  (PROG NIL
   LOOP (COND ((NULL VARS) (RETURN WFF)))
	(COND ((ATOM (CAR VARS)) (GO ATOM)))
	(COND ((EQUAL (CAAR VARS) (QUOTE CONS)) (GO DOT)))
	(ERREND (QUOTE (ILLEGAL ARGUMENT)))
   ATOM (SETQ WFF (EXGEN WFF (CAR VARS) (CAR VARS)))
	(GO ELOOP)
   DOT  (SETQ WFF (EXGEN WFF (CADAR VARS) (CADDAR VARS)))
   ELOOP
	(SETQ VARS (CDR VARS))
	(GO LOOP))) 
EXPR)

(DEFPROP EXGEN 
 (LAMBDA(WFF OLD NEW)
  (PROG (TEM)
	(SETQ TEM (GENSYM))
	(SETQ WFF (SUBST TEM OLD WFF))
	(COND
	 ((MEMBER NEW (ALLVARS WFF))
	  (ERREND (QUOTE (NEW VARIABLE CONFLICTS)))))
	(RETURN
	 (LIST (LIST (QUOTE THEREEXISTS) NEW)
	       (SUBST NEW TEM WFF))))) 
EXPR)

(DEFPROP EQI1 
 (LAMBDA(WFF1 WFF2)
  ((LAMBDA(W)
    (COND ((NOT (VALID W)) (QUOTE INVALID))
	  (T (SUBLIS W (QUOTE (EQUIVALENT PPP QQQ))))))
   (INST (CONS WFF1 WFF2)
	 (QUOTE ((IMPLIES PPP QQQ) IMPLIES QQQ PPP))
 	 NIL))) 
EXPR)

(DEFPROP ERREND 
 (LAMBDA (MESSAGE) (PROG NIL (PRINT MESSAGE) (ERR))) 
EXPR)

(DEFPROP FREEIN 
 (LAMBDA(VAR LINES)
  (COND ((NULL LINES) NIL)
	((MEMBER VAR (FREEVARS (WFFPART (CAR LINES)))) T)
	(T (FREEIN VAR (CDR LINES))))) 
EXPR)

(DEFPROP FREEVARS 
 (LAMBDA (EXPRESSION) (FREEVARS1 NIL NIL EXPRESSION)) 
EXPR)

(DEFPROP FREEVARS1 
 (LAMBDA(BVARS FVARS EXP)
  (COND
   ((ATOM EXP)
    (COND
     ((ISVAR EXP)
      (COND ((MEMBER EXP BVARS) FVARS)
	    ((MEMBER EXP FVARS) FVARS)
	    (T (CONS EXP FVARS))))
     (T FVARS)))
   ((ATOM (CAR EXP)) (FREEVARS2 BVARS FVARS (CDR EXP)))
   ((ATOM (CAAR EXP))
    (COND
     ((MEMBER (CAAR EXP) (QUOTE (FORALL THEREEXISTS)))
      (FREEVARS1 (CONS (CADAR EXP) BVARS) FVARS (CADDR EXP)))))
   (T (ERREND (QUOTE (UNKNOWN NONATOMIC FUNCTION)))))) 
EXPR)

(DEFPROP FREEVARS2 
 (LAMBDA(BVARS FVARS EXPL)
  (COND ((NULL EXPL) FVARS)
	(T
	 (FREEVARS1 BVARS
		    (FREEVARS2 BVARS FVARS (CDR EXPL))
		    (CAR EXPL))))) 
EXPR)

(DEFPROP GETCURLINE 
 (LAMBDA NIL (GETLINE (CURLINE))) 
EXPR)

(DEFPROP GETLINE 
 (LAMBDA(LINENO)
  (PROG (TEM)
	(SETQ TEM (ASSOC LINENO (CURTEXT)))
	(COND ((NULL TEM) (ERREND (QUOTE (NO SUCH LINE)))))
	(RETURN TEM))) 
EXPR)

(DEFPROP GIVEPROOF 
 (LAMBDA(L)
  (PROG NIL
	(COND
	 ((NOT (ATOM (CAR L)))
	  (ERREND (QUOTE (NON ATOMIC PROOF NAME)))))
	(COND
	 ((NOT (MEMBER (CAR L) PROOFS))
	  (SETQ PROOFS (APPEND PROOFS (LIST (CAR L))))))
	(PUTPROP (CAR L) (CADR L) (QUOTE PROOF)))) 
FEXPR)

(DEFPROP IFE1 
 (LAMBDA(WFF1 WFF2)
  ((LAMBDA(W X Y Z)
    (COND ((VALID W) (SUBLIS W (QUOTE QQQ)))
	  ((VALID X) (SUBLIS X (QUOTE RRR)))
	  ((VALID Y) (SUBLIS Y (QUOTE QQQ)))
	  ((VALID Z) (SUBLIS Z (QUOTE RRR)))
	  (T (QUOTE INVALID))))
   (INST (CONS WFF1 WFF2) (QUOTE (PPP COND (PPP QQQ) (T RRR))) NIL)
   (INST (CONS WFF1 WFF2)
	 (QUOTE ((NOT PPP) COND (PPP QQQ) (T RRR)))
 	 NIL)
   (INST (CONS WFF2 WFF1) (QUOTE (PPP COND (PPP QQQ) (T RRR))) NIL)
   (INST (CONS WFF2 WFF1)
	 (QUOTE ((NOT PPP) COND (PPP QQQ) (T RRR)))
 	 NIL))) 
EXPR)

(DEFPROP IFI1 
 (LAMBDA(WFF1 WFF2)
  ((LAMBDA(W X)
    (COND ((VALID W) (SUBLIS W (QUOTE (COND (PPP QQQ) (T RRR)))))
	  ((VALID X) (SUBLIS X (QUOTE (COND (PPP QQQ) (T RRR)))))
	  (T (QUOTE INVALID))))
   (INST (CONS WFF1 WFF2)
	 (QUOTE ((IMPLIES PPP QQQ) IMPLIES (NOT PPP) RRR))
 	 NIL)
   (INST (CONS WFF2 WFF1)
	 (QUOTE ((IMPLIES PPP QQQ) IMPLIES (NOT PPP) RRR))
 	 NIL))) 
EXPR)

(DEFPROP INITALL 
 (LAMBDA NIL
  (PROG NIL
	(SETQ CURPRF NIL)
	(SETQ AXIOMS NIL)
	(SETQ THEOREMS NIL)
	(SETQ PROOFS NIL)
	(SETQ SCHEMAS NIL))) 
EXPR)

(DEFPROP INITOPS 
 (LAMBDA NIL
  (PROG (INCR OP PREC PRECLIS)
	(SETQ PRECLIS
	      (CONS (QUOTE *COMMA*) (CONS (QUOTE SETQ) PRECLIS*)))
   LOOP (COND ((NULL PRECLIS) (RETURN NIL)))
	(SETQ OP (CAR PRECLIS))
	(SETQ PREC (GET OP (QUOTE INFIX)))
	(SETQ INCR
	      (COND ((GET OP (QUOTE LEFT)) (MINUS 1.)) (T 1.)))
	(PUTPROP OP
		 (LIST (PLUS (TIMES 3. PREC) INCR)
		       (DIFFERENCE (TIMES 3. PREC) INCR))
		 (QUOTE PREC))
	(SETQ PRECLIS (CDR PRECLIS))
	(GO LOOP))) 
EXPR)

(DEFPROP INITPROOF 
 (LAMBDA(NAME)
  (PROG NIL
	(COND
	 ((NULL NAME)
	  (ERREND (QUOTE (NIL NOT ACCEPTABLE PROOF NAME)))))
	(SETQ CURPRF NAME)
	(COND ((GETL NAME (QUOTE (PROOF))) (GO EXIST)))
	(PUTPROP NAME NIL (QUOTE PROOF))
	(SETQ PROOFS (APPEND PROOFS (LIST NAME)))
   EXIST
	(SETQ CURLIN
	      (COND ((NULL (CURTEXT)) 0.)
		    (T (CAAR (LAST (CURTEXT))))))
	(PUTPROP (QUOTE /@) (CURLINE) (QUOTE NEWNAM)))) 
EXPR)

(DEFPROP INITSTANCHARSET 
 (LAMBDA NIL
  (PROG NIL
	(PUTPROP (QUOTE AND) (QUOTE ∧) (QUOTE INFXNAM))
	(PUTPROP (QUOTE CMAPS) (QUOTE →→) (QUOTE INFXNAM))
	(PUTPROP (QUOTE *COMMA*) (QUOTE /,) (QUOTE INFXNAM))
	(PUTPROP (QUOTE CONS) (QUOTE /.) (QUOTE INFXNAM))
	(PUTPROP (QUOTE CONTAINED) (QUOTE ⊂) (QUOTE INFXNAM))
	(PUTPROP (QUOTE DIFFERENCE) (QUOTE /-) (QUOTE INFXNAM))
	(PUTPROP (QUOTE EQUAL) (QUOTE =) (QUOTE INFXNAM))
	(PUTPROP (QUOTE EQUIVALENT) (QUOTE ≡) (QUOTE INFXNAM))
	(PUTPROP (QUOTE EXPT) (QUOTE ↑) (QUOTE INFXNAM))
	(PUTPROP (QUOTE FORALL) (QUOTE ∀) (QUOTE INFXNAM))
	(PUTPROP (QUOTE GEQ) (QUOTE ≥) (QUOTE INFXNAM))
	(PUTPROP (QUOTE GREATERP) (QUOTE >) (QUOTE INFXNAM))
	(PUTPROP (QUOTE IMPLIES) (QUOTE ⊃) (QUOTE INFXNAM))
	(PUTPROP (QUOTE INTERSECTION) (QUOTE ∩) (QUOTE INFXNAM))
	(PUTPROP (QUOTE LAMBDA) (QUOTE λ) (QUOTE INFXNAM))
	(PUTPROP (QUOTE LEQ) (QUOTE ≤) (QUOTE INFXNAM))
	(PUTPROP (QUOTE LESSP) (QUOTE <) (QUOTE INFXNAM))
	(PUTPROP (QUOTE MAPS) (QUOTE →) (QUOTE INFXNAM))
	(PUTPROP (QUOTE MEMBER) (QUOTE ε) (QUOTE INFXNAM))
	(PUTPROP (QUOTE MINUS) (QUOTE /-) (QUOTE INFXNAM))
	(PUTPROP (QUOTE NEQ) (QUOTE ≠) (QUOTE INFXNAM))
	(PUTPROP (QUOTE NOT) (QUOTE ¬) (QUOTE INFXNAM))
	(PUTPROP (QUOTE OR) (QUOTE ∨) (QUOTE INFXNAM))
	(PUTPROP (QUOTE PLUS) (QUOTE /+) (QUOTE INFXNAM))
	(PUTPROP (QUOTE PRODUCT) (QUOTE ⊗) (QUOTE INFXNAM))
	(PUTPROP (QUOTE QUOTE) (QUOTE ') (QUOTE INFXNAM))
	(PUTPROP (QUOTE QUOTIENT) (QUOTE //) (QUOTE INFXNAM))
	(PUTPROP (QUOTE SETQ) (QUOTE ←) (QUOTE INFXNAM))
	(PUTPROP (QUOTE THEREEXISTS) (QUOTE ∃) (QUOTE INFXNAM))
	(PUTPROP (QUOTE TIMES) (QUOTE *) (QUOTE INFXNAM))
	(PUTPROP (QUOTE UNION) (QUOTE ∪) (QUOTE INFXNAM)))) 
EXPR)

(DEFPROP INITTTYCHARSET 
 (LAMBDA NIL
  (PROG NIL
	(PUTPROP (QUOTE AND) (QUOTE &) (QUOTE INFXNAM))
	(PUTPROP (QUOTE CMAPS) (QUOTE / CMAPS/ ) (QUOTE INFXNAM))
	(PUTPROP (QUOTE *COMMA*) (QUOTE /,) (QUOTE INFXNAM))
	(PUTPROP (QUOTE CONS) (QUOTE /.) (QUOTE INFXNAM))
	(PUTPROP (QUOTE CONTAINED)
		 (QUOTE / CONT/ )
		 (QUOTE INFXNAM))
	(PUTPROP (QUOTE DIFFERENCE) (QUOTE /-) (QUOTE INFXNAM))
	(PUTPROP (QUOTE EQUAL) (QUOTE =) (QUOTE INFXNAM))
	(PUTPROP (QUOTE EQUIVALENT) (QUOTE <=>) (QUOTE INFXNAM))
	(PUTPROP (QUOTE EXPT) (QUOTE ↑) (QUOTE INFXNAM))
	(PUTPROP (QUOTE FORALL) (QUOTE A) (QUOTE INFXNAM))
	(PUTPROP (QUOTE GEQ) (QUOTE >=) (QUOTE INFXNAM))
	(PUTPROP (QUOTE GREATERP) (QUOTE >) (QUOTE INFXNAM))
	(PUTPROP (QUOTE IMPLIES) (QUOTE =>) (QUOTE INFXNAM))
	(PUTPROP (QUOTE INTERSECTION)
		 (QUOTE / INTERSECT/ )
		 (QUOTE INFXNAM))
	(PUTPROP (QUOTE LAMBDA) (QUOTE L) (QUOTE INFXNAM))
	(PUTPROP (QUOTE LEQ) (QUOTE <=) (QUOTE INFXNAM))
	(PUTPROP (QUOTE LESSP) (QUOTE <) (QUOTE INFXNAM))
	(PUTPROP (QUOTE MAPS) (QUOTE / MAPS/ ) (QUOTE INFXNAM))
	(PUTPROP (QUOTE MEMBER) (QUOTE / MEMBER/ ) (QUOTE INFXNAM))
	(PUTPROP (QUOTE MINUS) (QUOTE /-) (QUOTE INFXNAM))
	(PUTPROP (QUOTE NEQ) (QUOTE / NEQ/ ) (QUOTE INFXNAM))
	(PUTPROP (QUOTE NOT) (QUOTE /-) (QUOTE INFXNAM))
	(PUTPROP (QUOTE OR) (QUOTE / V/ ) (QUOTE INFXNAM))
	(PUTPROP (QUOTE PLUS) (QUOTE /+) (QUOTE INFXNAM))
	(PUTPROP (QUOTE PRODUCT) (QUOTE / PROD/ ) (QUOTE INFXNAM))
	(PUTPROP (QUOTE QUOTE) (QUOTE ') (QUOTE INFXNAM))
	(PUTPROP (QUOTE QUOTIENT) (QUOTE //) (QUOTE INFXNAM))
	(PUTPROP (QUOTE SETQ) (QUOTE ←) (QUOTE INFXNAM))
	(PUTPROP (QUOTE THEREEXISTS) (QUOTE E) (QUOTE INFXNAM))
	(PUTPROP (QUOTE TIMES) (QUOTE *) (QUOTE INFXNAM))
	(PUTPROP (QUOTE UNION) (QUOTE / UNION/ ) (QUOTE INFXNAM)))) 
EXPR)

(DEFPROP INST 
 (LAMBDA(EXP MODEL PAIRS)
  (COND ((NOT (VALID PAIRS)) (QUOTE INVALID))
	((ATOM MODEL)
	 (COND
	  ((MEMBER MODEL (QUOTE (PPP QQQ RRR SSS)))
	   ((LAMBDA(W)
	     (COND ((NULL W) (CONS (CONS MODEL EXP) PAIRS))
		   ((EQUAL (CDR W) EXP) PAIRS)
		   (T (QUOTE INVALID))))
	    (ASSOC MODEL PAIRS)))
	  ((EQ MODEL EXP) PAIRS)
	  (T (QUOTE INVALID))))
	((ATOM EXP) (QUOTE INVALID))
	(T
	 (INST (CDR EXP)
	       (CDR MODEL)
	       (INST (CAR EXP) (CAR MODEL) PAIRS))))) 
EXPR)

(DEFPROP ISCONST 
 (LAMBDA (X) (OR (NUMBERP X) (MEMBER X LOGICALCONSTANTS))) 
EXPR)

(DEFPROP ISEQUIVALENCE 
 (LAMBDA (WFF) (MEMBER WFF (QUOTE (EQUAL EQUIVALENT SETQ)))) 
EXPR)

(DEFPROP ISIDENT 
 (LAMBDA (X) (AND (ATOM X) (NOT (NUMBERP X)))) 
EXPR)

(DEFPROP ISQUANT 
 (LAMBDA (X) (MEMBER X QUANTIFIERS)) 
EXPR)

(DEFPROP ISVAR 
 (LAMBDA (X) (AND (ISIDENT X) (NOT (ISCONST X)))) 
EXPR)

(DEFPROP LAMEXP 
 (LAMBDA(FORMULA)
  (COND ((ATOM FORMULA) FORMULA)
	((ATOM (CAR FORMULA))
	 (CONS (CAR FORMULA) (LAMEXPL (CDR FORMULA))))
	((EQUAL (CAAAR FORMULA) (QUOTE LAMBDA))
	 (PROPSUBST (CADR FORMULA)
		    (CADAAR FORMULA)
		    (CADAR FORMULA)))
	(T (CONS (LAMEXP (CAR FORMULA)) (LAMEXPL (CDR FORMULA)))))) 
EXPR)

(DEFPROP LAMEXPL 
 (LAMBDA (LIST) (MAPCAR (FUNCTION LAMEXP) LIST)) 
EXPR)

(DEFPROP MAKECONSES 
 (LAMBDA(L)
  (PROG (RES)
   LOOP (COND ((NULL L) (RETURN RES)))
	(COND
	 ((OR (ATOM (CAR L))
	      (NEQ (CAAR L) (QUOTE CONS))
	      (NEQ (LENGTH (CAR L)) 3.))
	  (ERREND (QUOTE (BAD ARGUMENT)))))
	(SETQ RES (CONS (CONS (CADAR L) (CADDAR L)) RES))
	(SETQ L (CDR L))
	(GO LOOP))) 
EXPR)

(DEFPROP MAKERNL 
 (LAMBDA(FREEV ALLV)
  (PROG (CNT ID NVAR NEWVARS VAR)
   LOOP (COND ((NULL FREEV) (RETURN NEWVARS)))
	(SETQ VAR (CAR FREEV))
	(COND ((MEMBER VAR ALLV) (GO MAKE)))
   ELOOP
	(SETQ FREEV (CDR FREEV))
	(GO LOOP)
   MAKE (SETQ ID (ALPHAPART VAR))
	(SETQ CNT 1.)
   MAKE1
	(SETQ NVAR (MAKESYM ID CNT))
	(COND ((MEMBER NVAR ALLV) (GO EMAKE)))
	(SETQ NEWVARS (CONS (CONS VAR NVAR) NEWVARS))
	(GO ELOOP)
   EMAKE
	(SETQ CNT (PLUS CNT 1.))
	(GO MAKE1))) 
EXPR)

(DEFPROP MAKEVAR 
 (LAMBDA(V L)
  (PROG (TEM)
	(SETQ TEM (MAKERNL (LIST V) L))
	(RETURN (COND ((NULL TEM) V) (T (CDAR TEM)))))) 
EXPR)

(DEFPROP MAKESYM 
 (LAMBDA(IDENT NUM)
  (READLIST (APPEND (EXPLODE IDENT) (EXPLODE NUM)))) 
EXPR)

(DEFPROP MAKETHEOREM1 
 (LAMBDA(THEOREM LINE PROOF)
  (PROG NIL
	(INITPROOF PROOF)
	(COND
	 ((NOT (NULL (ASSPART LINE)))
	  (ERREND (QUOTE (STILL HAS ASSUMPTIONS)))))
	(PUTPROP THEOREM (WFFPART LINE) (QUOTE THEOREM))
	(PUTPROP THEOREM (LIST LINE PROOF) (QUOTE BY))
	(SETQ THEOREMS (APPEND THEOREMS (LIST THEOREM)))
	(COND (*PRINT (SHOWTHEOREM THEOREM))))) 
EXPR)

(DEFPROP MP1 
 (LAMBDA(U V)
  (PROG (W)
	(SETQ W
	      (INST (CONS U V) (QUOTE (PPP IMPLIES PPP QQQ)) NIL))
	(COND
	 ((NOT (VALID W))
	  (SETQ W
		(INST (CONS V U)
		      (QUOTE (PPP IMPLIES PPP QQQ))
 		      NIL))))
	(COND
	 ((NOT (VALID W)) (RETURN (QUOTE INVALID)))
	 (T (RETURN (SUBLIS W (QUOTE QQQ))))))) 
EXPR)

(DEFPROP NEXTLINE 
 (LAMBDA NIL (PLUS (CURLINE) 1.)) 
EXPR)

(DEFPROP NOTELIM 
 (LAMBDA(X NOTX)
  ((LAMBDA (X Y) (COND ((NOT (VALID X)) Y) (T X)))
   (INST (CONS X NOTX) (QUOTE (PPP NOT PPP)) NIL)
   (INST (CONS NOTX X) (QUOTE (PPP NOT PPP)) NIL))) 
EXPR)

(DEFPROP NOTINTRO 
 (LAMBDA(PROP)
  ((LAMBDA(W)
    (COND ((NOT (VALID W)) (QUOTE INVALID))
	  (T (SUBLIS W (QUOTE (NOT PPP))))))
   (INST PROP (QUOTE (IMPLIES PPP FALSE)) NIL))) 
EXPR)

(DEFPROP NTHCDR 
 (LAMBDA(L N)
  (COND ((EQUAL N 0.) L) (T (NTHCDR (CDR L) (DIFFERENCE N 1.))))) 
EXPR)

(DEFPROP NTHELT 
 (LAMBDA (L N) (CAR (NTHCDR L (DIFFERENCE N 1.)))) 
EXPR)

(DEFPROP NUMPART 
 (LAMBDA (LINE) (CAR (GETLINE LINE))) 
EXPR)

(DEFPROP ORELIM1 
 (LAMBDA(DISJUN IMPS)
  (PROG (ANTECEDS PREMS RES)
	(COND
	 ((NEQ (CAR DISJUN) (QUOTE OR))
	  (ERREND (QUOTE (FIRST ARG MUST BE DISJUNCTION)))))
	(COND
	 ((NULL (CDR DISJUN)) (ERREND (QUOTE (NO DISJUNCTS)))))
	(COND
	 ((NULL IMPS)
	  (ERREND (QUOTE (NEED AT LEAST ONE IMPLICATION)))))
	(SETQ PREMS (CDR DISJUN))
	(SETQ RES (CDDAR IMPS))
   LOOP1
	(COND
	 ((NEQ (CAAR IMPS) (QUOTE IMPLIES))
	  (ERREND (QUOTE (ARG NOT IMPLICATION)))))
	(COND
	 ((NEQ (CDDAR IMPS) RES)
	  (ERREND (QUOTE (MULTIPLE CONCLUSIONS)))))
	(SETQ ANTECEDS (CONS (CADAR IMPS) ANTECEDS))
	(COND ((NOT (NULL (SETQ IMPS (CDR IMPS)))) (GO LOOP1)))
   LOOP2
	(COND ((NULL PREMS) (RETURN (CAR RES))))
	(COND
	 ((NOT (MEMBER (CAR PREMS) ANTECEDS))
	  (ERREND (QUOTE (UNPROVEN DISJUNCT)))))
	(SETQ PREMS (CDR PREMS))
	(GO LOOP2))) 
EXPR)

(DEFPROP PCERR 
 (LAMBDA NIL
  (PROG NIL
	(PRINC (QUOTE PROOF/ CHECKER))
	(LINELENGTH CONSOLEWIDTH)
	(PROG NIL (SETQ *FILEPRINT NIL))
	(PROG NIL (SETQ *PRINT T))
	(PROG NIL (SETQ *TWODIM NIL))
	(EVAL (QUOTE (BEGIN))))) 
EXPR)

(DEFPROP PCINIT 
 (LAMBDA NIL
  (PROG NIL
	(EXCISE)
	(ONDD)
	(INITOPS)
	(INITALL)
	(INITFN (QUOTE PCSTART))
	(PRINC (QUOTE PROOF/ CHECKER/ INITIALIZED)))) 
EXPR)

(DEFPROP PCSTART 
 (LAMBDA NIL
  (PROG NIL
	(ERRSET (RESTOREALL (CONS PCHECK INI)) NIL)
	(INITFN (QUOTE PCERR))
	(PCERR))) 
EXPR)

(DEFPROP PAIRLIS 
 (LAMBDA(CARS CDRS)
  (COND ((OR (NULL CARS) (NULL CDRS)) NIL)
	(T
	 (CONS (CONS (CAR CARS) (CAR CDRS))
	       (PAIRLIS (CDR CARS) (CDR CDRS)))))) 
EXPR)

(DEFPROP PROPSUBST 
 (LAMBDA(TERM VAR EXP)
  (PROPSUBST1 TERM
 	      VAR
 	      EXP
	      (MAKERNL (FREEVARS TERM) (ALLVARS EXP)))) 
EXPR)

(DEFPROP PROPSUBST1 
 (LAMBDA(TERM VAR EXP RNL)
  (COND
   ((ATOM EXP)
    (COND ((ISVAR EXP) (COND ((EQUAL EXP VAR) TERM) (T EXP)))
	  (T EXP)))
   ((AND (NOT (ATOM (CAR EXP))) (ISQUANT (CAAR EXP)))
    (COND ((EQUAL (CADAR EXP) VAR) EXP)
	  (T
	   (PROG (NEWNAM)
		 (SETQ NEWNAM (ASSOC (CADAR EXP) RNL))
		 (SETQ NEWNAM
		       (COND
			((NULL NEWNAM) (CADAR EXP))
			(T (CDR NEWNAM))))
		 (RETURN
		  (LIST (LIST (CAAR EXP) NEWNAM)
			(PROPSUBST1 TERM
 				    VAR
				    (SUBST NEWNAM
					   (CADAR EXP)
					   (CADR EXP))
 				    RNL)))))))
   (T
    (CONS (PROPSUBST1 TERM VAR (CAR EXP) RNL)
	  (PROPSUBSTL TERM VAR (CDR EXP) RNL))))) 
EXPR)

(DEFPROP PROPSUBSTL 
 (LAMBDA(TERM VAR EXPL RNL)
  (COND ((NULL EXPL) NIL)
	(T
	 (CONS (PROPSUBST1 TERM VAR (CAR EXPL) RNL)
	       (PROPSUBSTL TERM VAR (CDR EXPL) RNL))))) 
EXPR)

(DEFPROP QUANTEQUIV 
 (LAMBDA(EXP1 CONT1 EXP2 CONT2)
  (PROG (GEN TEM)
	(COND ((ATOM EXP1) (GO ATOM)))
	(COND ((ATOM EXP2) (RETURN NIL)))
	(COND ((ATOM (CAR EXP1)) (GO FUN)))
	(COND ((ISQUANT (CAAR EXP1)) (GO QUANT)))
   LIST (COND ((NULL EXP1) (RETURN (NULL EXP2))))
	(COND
	 ((NOT (QUANTEQUIV (CAR EXP1) CONT1 (CAR EXP2) CONT2))
	  (RETURN NIL)))
	(SETQ EXP1 (CDR EXP1))
	(SETQ EXP2 (CDR EXP2))
	(GO LIST)
   ATOM (SETQ TEM (ASSOC EXP1 CONT1))
	(COND ((NOT (NULL TEM)) (SETQ EXP1 (CDAR TEM))))
	(SETQ TEM (ASSOC EXP2 CONT2))
	(COND ((NOT (NULL TEM)) (SETQ EXP1 (CDAR TEM))))
	(RETURN (EQUAL EXP1 EXP2))
   FUN  (COND ((NEQ (CAR EXP1) (CAR EXP2)) (RETURN NIL)))
	(SETQ EXP1 (CDR EXP1))
	(SETQ EXP2 (CDR EXP2))
	(GO LIST)
   QUANT
	(COND
	 ((OR (ATOM (CAR EXP2))
	      (NOT (ISQUANT (CAAR EXP2)))
	      (NEQ (CAAR EXP1) (CAAR EXP2)))
	  (RETURN NIL)))
	(SETQ GEN (GENSYM))
	(RETURN
	 (QUANTEQUIV (CADR EXP1)
		     (CONS (CONS (CADAR EXP1) GEN) CONT1)
		     (CADR EXP2)
		     (CONS (CONS (CADAR EXP2) GEN) CONT2))))) 
EXPR)

(DEFPROP REPEITHER 
 (LAMBDA(WFF EQUAT FLAG ORD)
  (COND
   ((NOT (ISEQUIVALENCE (CAR EQUAT)))
    (ERREND (QUOTE (NO EQUATION))))
   (T
    (REPNTH (COND (FLAG (CADDR EQUAT)) (T (CADR EQUAT)))
	    (COND (FLAG (CADR EQUAT)) (T (CADDR EQUAT)))
 	    WFF
 	    ORD)))) 
EXPR)

(DEFPROP REPNTH 
 (LAMBDA(NEW OLD EXP NUM)
  (PROG (NEWEXP ORDCNT)
	(SETQ ORDCNT 0.)
	(SETQ NEWEXP (REPNTH1 NEW OLD EXP NIL NUM))
	(COND
	 ((LESSP ORDCNT NUM) (ERREND (QUOTE (NO REPLACEMENT)))))
	(RETURN NEWEXP))) 
EXPR)

(DEFPROP REPNTH1 
 (LAMBDA(NEXP OEXP EXP CON NUM)
  (PROG (BVAR GEN NVAR)
	(COND ((QUANTEQUIV OEXP NIL EXP CON) (GO GOTIT)))
	(COND ((ATOM EXP) (RETURN EXP)))
	(COND
	 ((ATOM (CAR EXP))
	  (RETURN
	   (CONS (CAR EXP)
		 (REPNTHL NEXP OEXP (CDR EXP) CON NUM)))))
	(COND ((ISQUANT (CAAR EXP)) (GO QUANT)))
   QUANT
	(SETQ GEN (GENSYM))
	(SETQ BVAR (CADAR EXP))
	(SETQ NVAR
	      (COND
	       ((MEMBER BVAR (ALLVARS NEXP))
		(MAKEVAR BVAR (ALLVARS (CADR EXP))))
	       (T BVAR)))
	(RETURN
	 (LIST (LIST (CAAR EXP) NVAR)
	       (REPNTH1 NEXP
 			OEXP
			(SUBST NVAR BVAR (CADR EXP))
			(CONS (CONS NVAR GEN) CON)
 			NUM)))
   GOTIT
	(SETQ ORDCNT (PLUS ORDCNT 1.))
	(RETURN (COND ((EQUAL ORDCNT NUM) NEXP) (T EXP))))) 
EXPR)

(DEFPROP REPNTHL 
 (LAMBDA(NEXP OEXP LST CON NUM)
  (COND ((NULL LST) NIL)
	(T
	 (CONS (REPNTH1 NEXP OEXP (CAR LST) CON NUM)
	       (REPNTHL NEXP OEXP (CDR LST) CON NUM))))) 
EXPR)

(DEFPROP SAVEAXIOM 
 (LAMBDA(AXIOM)
  (PRINTEXPR
   (LIST (QUOTE ADDAXIOM) AXIOM (GET AXIOM (QUOTE AXIOM))))) 
EXPR)

(DEFPROP SAVEAXCOM 
 (LAMBDA(AXIOM)
  (PRINTEXPR
   (LIST (QUOTE GIVEAX) AXIOM (GET AXIOM (QUOTE AXIOM))))) 
EXPR)

(DEFPROP SAVEPRFCOM 
 (LAMBDA(PROOF)
  (PROG (PRF)
	(PRINT (LIST (QUOTE PROOF) PROOF))
	(SETQ PRF (GET PROOF (QUOTE PROOF)))
   LOOP (COND ((NULL PRF) (RETURN (TERPRI))))
	(COND
	 ((EQUAL (CAR (CADDR (CAR PRF))) (QUOTE USETHM))
	  (SAVETHMCOM (CADR (CADDR (CAR PRF))))))
	(PRINT (CAAR PRF))
	(PRINC (QUOTE /	))
	(PRINTSUBEXPR (CADDR (CAR PRF)) 9. 0.)
	(SETQ PRF (CDR PRF))
	(GO LOOP))) 
EXPR)

(DEFPROP SAVEPROOF 
 (LAMBDA(PROOF)
  (PRINTEXPR
   (LIST (QUOTE GIVEPROOF) PROOF (GET PROOF (QUOTE PROOF))))) 
EXPR)

(DEFPROP SAVESCHEMA 
 (LAMBDA(SCHEMA)
  (PRINTEXPR
   (LIST (QUOTE ADDSCHEMA) SCHEMA (GET SCHEMA (QUOTE SCHEMA))))) 
EXPR)

(DEFPROP SAVESCHMCOM 
 (LAMBDA(SCHEMA)
  (PRINTEXPR
   (LIST (QUOTE GIVESCHM) SCHEMA (GET SCHEMA (QUOTE SCHEMA))))) 
EXPR)

(DEFPROP SAVETHEOREM 
 (LAMBDA(THEOREM)
  (PRINTEXPR
   (LIST (QUOTE ADDTHM)
 	 THEOREM
	 (CAR (GET THEOREM (QUOTE BY)))
	 (CADR (GET THEOREM (QUOTE BY)))))) 
EXPR)

(DEFPROP SAVETHMCOM 
 (LAMBDA(THEOREM)
  (PRINTEXPR
   (LIST (QUOTE MAKETHM)
 	 THEOREM
	 (CAR (GET THEOREM (QUOTE BY)))
	 (CADR (GET THEOREM (QUOTE BY)))))) 
EXPR)

(DEFPROP SETDIF 
 (LAMBDA(X Y)
  (PROG (ANS)
   LOOP (COND ((NULL X) (RETURN (REVERSE ANS))))
	(COND
	 ((NOT (MEMBER (CAR X) Y)) (SETQ ANS (CONS (CAR X) ANS))))
	(SETQ X (CDR X))
	(GO LOOP))) 
EXPR)

(DEFPROP SHOWAXIOM 
 (LAMBDA(NAME)
  (PROG NIL
	(PRINT (QUOTE AXIOM))
	(PRINC NAME)
	(TERPRI)
	(SHOWEXP (GET NAME (QUOTE AXIOM)))
	(TERPRI))) 
EXPR)

(DEFPROP SHOWCURLINE 
 (LAMBDA NIL
  (COND ((EQUAL (CURLINE) 0.) (SHOW)) (T (SHOWLINE (GETCURLINE))))) 
EXPR)

(DEFPROP SHOWEXP 
 (LAMBDA(EXP)
  (COND (*TWODIM (TDDEXP EXP (CURCOL) 0.)) (T (INFX EXP)))) 
EXPR)

(DEFPROP SHOWLINE 
 (LAMBDA(LINTXT)
  (PROG (COM)
	(TERPRI)
	(TERPRI)
	(PRINC (CAR LINTXT))
	(PRINC (QUOTE :))
	(PRINC (QUOTE /	))
	(SHOWEXP (CADR LINTXT))
	(PRINS (QUOTE BY))
	(SETQ COM (CADDR LINTXT))
	(COND ((EQUAL (CAR COM) (QUOTE ASS)) (GO ASS)))
	(COND
	 ((EQUAL (CAR COM) (QUOTE USEAX))
	  (SETQ COM (CONS (QUOTE AXIOM) (CDR COM)))))
	(COND
	 ((EQUAL (CAR COM) (QUOTE USESCHM))
	  (SETQ COM (CONS (QUOTE SCHEMA) (CDR COM)))))
	(COND
	 ((EQUAL (CAR COM) (QUOTE USETHM))
	  (SETQ COM (CONS (QUOTE THEOREM) (CDR COM)))))
	(SHOWEXP COM)
	(COND ((NULL (CADDDR LINTXT)) (RETURN NIL)))
	(PRINS (QUOTE ASSUMING))
	(PRINS (CADDDR LINTXT))
	(RETURN NIL)
   ASS  (PRINS (QUOTE ASSUMPTION)))) 
EXPR)

(DEFPROP SHOWPROOF 
 (LAMBDA(NAME)
  (PROG NIL
	(PRINT (QUOTE PROOF))
	(PRINS NAME)
	(MAPC (FUNCTION SHOWLINE) (GET NAME (QUOTE PROOF)))
	(TERPRI))) 
EXPR)

(DEFPROP SHOWSCHEMA 
 (LAMBDA(NAME)
  (PROG NIL
	(PRINT (QUOTE SCHEMA))
	(PRINC NAME)
	(TERPRI)
	(SHOWEXP (GET NAME (QUOTE SCHEMA)))
	(TERPRI))) 
EXPR)

(DEFPROP SHOWTHEOREM 
 (LAMBDA(NAME)
  (PROG NIL
	(PRINT (QUOTE THEOREM))
	(PRINS NAME)
	(TERPRI)
	(SHOWEXP (GET NAME (QUOTE THEOREM))))) 
EXPR)
 (DEFPROP AXIOM SHOWAXIOM IMAGE)

 (DEFPROP PROOF SHOWPROOF IMAGE)

 (DEFPROP SCHEMA SHOWSCHEMA IMAGE)

 (DEFPROP THEOREM SHOWTHEOREM IMAGE)


(DEFPROP SPECALL 
 (LAMBDA(FORM ARGS)
  (PROG NIL
   LOOP (COND ((NULL ARGS) (RETURN FORM)))
	(COND ((ATOM FORM) (ERREND (QUOTE (ATOMIC EXPRESSION)))))
	(COND
	 ((AND (NEQ (CAAR FORM) (QUOTE FORALL))
	       (NEQ (CAAR FORM) (QUOTE THEREEXISTS)))
	  (ERREND (QUOTE (NOT QUANTIFIED EXPRESSION)))))
	(RETURN
	 (SPECALL (PROPSUBST (CAR ARGS) (CADAR FORM) (CADR FORM))
		  (CDR ARGS))))) 
EXPR)

(DEFPROP TH1 
 (LAMBDA(A1 A2 A C)
  (COND ((NULL A) (TH2 A1 A2 NIL NIL C))
	(T
	 (OR (MEMBER (CAR A) C)
	     (COND
	      ((ATOM (CAR A))
	       (TH1 (COND ((MEMBER (CAR A) A1) A1)
			  (T (CONS (CAR A) A1)))
 		    A2
		    (CDR A)
 		    C))
	      (T
	       (TH1 A1
		    (COND ((MEMBER (CAR A) A2) A2)
			  (T (CONS (CAR A) A2)))
		    (CDR A)
 		    C))))))) 
EXPR)

(DEFPROP TH2 
 (LAMBDA(A1 A2 C1 C2 C)
  (COND ((NULL C) (TH A1 A2 C1 C2))
	((ATOM (CAR C))
	 (TH2 A1
 	      A2
	      (COND ((MEMBER (CAR C) C1) C1) (T (CONS (CAR C) C1)))
 	      C2
	      (CDR C)))
	(T
	 (TH2 A1
 	      A2
 	      C1
	      (COND ((MEMBER (CAR C) C2) C2) (T (CONS (CAR C) C2)))
	      (CDR C))))) 
EXPR)

(DEFPROP TH 
 (LAMBDA(A1 A2 C1 C2)
  (COND ((NULL A2)
	 (AND (NOT (NULL C2)) (THR (CAR C2) A1 A2 C1 (CDR C2))))
	(T (THL (CAR A2) A1 (CDR A2) C1 C2)))) 
EXPR)

(DEFPROP THL 
 (LAMBDA(U A1 A2 C1 C2)
  (COND ((EQUAL (CAR U) (QUOTE NOT)) (TH1R (CADR U) A1 A2 C1 C2))
	((EQUAL (CAR U) (QUOTE AND))
	 (TH2L (CDR (BINAND (CDR U))) A1 A2 C1 C2))
	((EQUAL (CAR U) (QUOTE OR))
	 (AND (TH1L (CADR (BINOR (CDR U))) A1 A2 C1 C2)
	      (TH1L (CADDR (BINOR (CDR U))) A1 A2 C1 C2)))
	((EQUAL (CAR U) (QUOTE IMPLIES))
	 (AND (TH1L (CADDR U) A1 A2 C1 C2)
	      (TH1R (CADR U) A1 A2 C1 C2)))
	((EQUAL (CAR U) (QUOTE EQUIVALENT))
	 (AND (TH2L (CDR U) A1 A2 C1 C2)
	      (TH2R (CDR U) A1 A2 C1 C2)))
	((MEMBER U C1) T)
	(T (TH (CONS U A1) A2 C1 C2)))) 
EXPR)

(DEFPROP THR 
 (LAMBDA(U A1 A2 C1 C2)
  (COND ((EQUAL (CAR U) (QUOTE NOT)) (TH1L (CADR U) A1 A2 C1 C2))
	((EQUAL (CAR U) (QUOTE AND))
	 (AND (TH1R (CADR U) A1 A2 C1 C2)
	      (TH1R (CADDR U) A1 A2 C1 C2)))
	((EQUAL (CAR U) (QUOTE OR)) (TH2R (CDR U) A1 A2 C1 C2))
	((EQUAL (CAR U) (QUOTE IMPLIES))
	 (TH11 (CDR U) A1 A2 C1 C2))
	((EQUAL (CAR U) (QUOTE EQUIVALENT))
	 (AND (TH11 (CDR U) A1 A2 C1 C2)
	      (TH11 (REVERSE (CDR U)) A1 A2 C1 C2)))
	((MEMBER U A1) T)
	(T (TH A1 A2 (CONS U C1) C2)))) 
EXPR)

(DEFPROP TH1L 
 (LAMBDA(V A1 A2 C1 C2)
  (COND ((ATOM V) (OR (MEMBER V C1) (TH (CONS V A1) A2 C1 C2)))
	(T (OR (MEMBER V C2) (TH A1 (CONS V A2) C1 C2))))) 
EXPR)

(DEFPROP TH1R 
 (LAMBDA(V A1 A2 C1 C2)
  (COND ((ATOM V) (OR (MEMBER V A1) (TH A1 A2 (CONS V C1) C2)))
	(T (OR (MEMBER V A2) (TH A1 A2 C1 (CONS V C2)))))) 
EXPR)

(DEFPROP TH2L 
 (LAMBDA(V A1 A2 C1 C2)
  (COND ((ATOM (CAR V))
	 (OR (MEMBER (CAR V) C1)
	     (TH1L (CADR V) (CONS (CAR V) A1) A2 C1 C2)))
	(T
	 (OR (MEMBER (CAR V) C2)
	     (TH1L (CADR V) A1 (CONS (CAR V) A2) C1 C2))))) 
EXPR)

(DEFPROP TH2R 
 (LAMBDA(V A1 A2 C1 C2)
  (COND ((ATOM (CAR V))
	 (OR (MEMBER (CAR V) A1)
	     (TH1R (CADR V) A1 A2 (CONS (CAR V) C1) C2)))
	(T
	 (OR (MEMBER (CAR V) A2)
	     (TH1R (CADR V) A1 A2 C1 (CONS (CAR V) C2)))))) 
EXPR)

(DEFPROP TH11 
 (LAMBDA(V A1 A2 C1 C2)
  (COND ((ATOM (CAR V))
	 (OR (MEMBER (CAR V) C1)
	     (TH1R (CADR V) (CONS (CAR V) A1) A2 C1 C2)))
	(T
	 (OR (MEMBER (CAR V) C2)
	     (TH1R (CADR V) A1 (CONS (CAR V) A2) C1 C2))))) 
EXPR)

(DEFPROP UNGEN 
 (LAMBDA(WFF ASS FVAR BVAR)
  (PROG (TEM)
	(COND
	 ((FREEIN FVAR ASS)
	  (ERREND (QUOTE (VARIABLE FREE IN ASSUMPTIONS)))))
	(COND
	 ((USEDINEXISTSPEC FVAR)
	  (ERREND (QUOTE (USED IN EXISTENTIALLY SPECIFIED LINE)))))
	(SETQ TEM (GENSYM))
	(SETQ WFF (SUBST TEM FVAR WFF))
	(COND
	 ((MEMBER BVAR (ALLVARS WFF))
	  (ERREND (QUOTE (VARIABLE CONFLICT)))))
	(RETURN
	 (LIST (LIST (QUOTE FORALL) BVAR) (SUBST BVAR TEM WFF))))) 
EXPR)

(DEFPROP UNION 
 (LAMBDA(SETS)
  (COND ((NULL SETS) NIL)
	((NULL (CDR SETS)) (CAR SETS))
	(T (UNION2 (CAR SETS) (UNION (CDR SETS)))))) 
EXPR)

(DEFPROP UNION2 
 (LAMBDA(SET1 SET2)
  (COND ((NULL SET1) SET2)
	((MEMBER (CAR SET1) SET2) (UNION2 (CDR SET1) SET2))
	(T (UNION2 (CDR SET1) (CONS (CAR SET1) SET2))))) 
EXPR)

(DEFPROP USEDINEXISTSPEC 
 (LAMBDA(VAR)
  (PROG (PRF)
	(SETQ PRF (CURTEXT))
   LOOP (COND ((NULL PRF) (RETURN NIL)))
	(COND
	 ((AND (EQUAL (CAR (CADDAR PRF)) (QUOTE ES))
	       (MEMBER VAR (FREEVARS (CADAR PRF))))
	  (RETURN T)))
	(SETQ PRF (CDR PRF))
	(GO LOOP))) 
EXPR)

(DEFPROP USEDVAR 
 (LAMBDA(VAR)
  (PROG (PRF)
	(SETQ PRF (CURTEXT))
   LOOP (COND ((NULL PRF) (RETURN NIL)))
	(COND ((MEMBER VAR (ALLVARS (CADAR PRF))) (RETURN T)))
	(SETQ PRF (CDR PRF))
	(GO LOOP))) 
EXPR)

(DEFPROP VALID 
 (LAMBDA (PROP) (NEQ PROP (QUOTE INVALID))) 
EXPR)

(DEFPROP WFFLIST 
 (LAMBDA (L) (MAPCAR (FUNCTION WFFPART) L)) 
EXPR)

(DEFPROP WFFPART 
 (LAMBDA (LINE) (CADR (GETLINE LINE))) 
EXPR)

(DEFPROP GETINFXNAM 
 (LAMBDA(ATOM)
  (PROG (NAME)
	(COND ((NUMBERP ATOM) (RETURN ATOM)))
	(SETQ NAME (SEEKPROP ATOM (QUOTE INFXNAM)))
	(COND ((NOT (NULL NAME)) (RETURN (PROPVAL NAME))))
	(RETURN ATOM))) 
EXPR)

(DEFPROP INFX 
 (LAMBDA(EXP)
  (PROG NIL (INFXEXPR EXP 0. 0.) (INFXATOM (QUOTE / )))) 
EXPR)

(DEFPROP INFXARGS 
 (LAMBDA(ARGS LPREC RPREC)
  (COND ((NULL ARGS)
	 (PROG NIL (INFXATOM (QUOTE /()) (INFXATOM (QUOTE /)))))
	((NULL (CDR ARGS))
	 (PROG NIL
	       (INFXATOM (QUOTE / ))
	       (INFXEXPR (CAR ARGS) LPREC RPREC)))
	(T (INFXPARENED (CONS (QUOTE *COMMA*) ARGS) LPREC RPREC)))) 
EXPR)
 (PUTPROP (QUOTE INFXATOM) (QUOTE PRNTATOM) (QUOTE EXPR))


(DEFPROP INFXCOND 
 (LAMBDA(S L R)
  (PROG NIL
	(INFXATOM (QUOTE IF))
	(INFXATOM (QUOTE / ))
	(INFXEXPR (CAADR S) 0. 0.)
	(INFXATOM (QUOTE / ))
	(INFXATOM (QUOTE THEN))
	(INFXATOM (QUOTE / ))
	(INFXEXPR (CADADR S) 0. 0.)
	(INFXATOM (QUOTE / ))
	(COND ((NULL (CDDR S)) (RETURN NIL)))
	(INFXATOM (QUOTE ELSE))
	(INFXATOM (QUOTE / ))
	(INFXEXPR (CADR (CADDR S)) 0. 0.))) 
EXPR)

(DEFPROP INFXFUN 
 (LAMBDA(FN LPREC RPREC)
  (COND ((ATOM FN) (INFXATOM FN))
	(T (INFXPARENED FN LPREC RPREC)))) 
EXPR)

(DEFPROP INFXEXPR 
 (LAMBDA(EXP LPREC RPREC)
  (PROG (OP)
	(COND ((ATOM EXP) (RETURN (INFXATOM EXP))))
	(COND ((NOT (ATOM (CAR EXP))) (GO NOATM)))
	(SETQ OP (GETGET (CAR EXP) (QUOTE INFXFUN)))
	(COND
	 ((NOT (NULL OP))
	  (RETURN (APPLY (PROPVAL OP) (LIST EXP LPREC RPREC)))))
   NOATM
	(INFXFUN (CAR EXP) LPREC RPREC)
	(INFXARGS (CDR EXP) 10000. RPREC))) 
EXPR)

(DEFPROP INFXLIST 
 (LAMBDA(OP ARGS LPREC RPREC)
  (PROG (PREC)
	(SETQ PREC (GET OP (QUOTE PREC)))
   LOOP (COND ((NULL ARGS) (RETURN NIL)))
	(INFXATOM OP)
	(INFXEXPR (CAR ARGS)
		  (CADR PREC)
		  (COND ((NULL (CDR ARGS)) RPREC) (T (CAR PREC))))
	(SETQ ARGS (CDR ARGS))
	(GO LOOP))) 
EXPR)

(DEFPROP INFXOPER 
 (LAMBDA(EXP LPREC RPREC)
  (PROG (PREC)
	(SETQ PREC (GET (CAR EXP) (QUOTE PREC)))
	(COND
	 ((OR (LESSP (CAR PREC) LPREC) (LESSP (CADR PREC) RPREC))
	  (RETURN (INFXPARENED EXP LPREC RPREC))))
	(COND ((NULL (CDR EXP)) (RETURN (INFXATOM (CAR EXP)))))
	(COND
	 ((NULL (CDDR EXP))
	  (RETURN (INFXLIST (CAR EXP) (CDR EXP) LPREC RPREC))))
	(INFXEXPR (CADR EXP) LPREC (CAR PREC))
	(RETURN (INFXLIST (CAR EXP) (CDDR EXP) LPREC RPREC)))) 
EXPR)

(DEFPROP INFXPARENED 
 (LAMBDA(EXP LPREC RPREC)
  (PROG NIL
	(INFXATOM (QUOTE /())
	(INFXEXPR EXP 0. 0.)
	(INFXATOM (QUOTE /))))) 
EXPR)

(DEFPROP INFXQUOTE 
 (LAMBDA(SEXPR LPREC RPREC)
  (PROG NIL (INFXATOM (QUOTE QUOTE)) (PRIN1 (CADR SEXPR)))) 
EXPR)

(DEFPROP INFXSPEC 
 (LAMBDA(SEXPR LPREC RPREC)
  ((GET (CAR SEXPR) (QUOTE SPECOPER)) SEXPR LPREC RPREC)) 
EXPR)

(DEFPROP PRNTATOM 
 (LAMBDA(AT)
  (PROG (NAM)
	(SETQ NAM (GETINFXNAM AT))
	(COND ((LESSP (CHRCT) (PLUS (FLATSIZE NAM) 1.)) (TERPRI)))
	(PRINC NAM))) 
EXPR)
 (PUTPROP (QUOTE PREC) (QUOTE INFXOPER) (QUOTE INFXFUN))

 (PUTPROP (QUOTE SPECOPER) (QUOTE INFXSPEC) (QUOTE INFXFUN))

 (PUTPROP (QUOTE COND) (QUOTE INFXCOND) (QUOTE SPECOPER))

 (PUTPROP (QUOTE QUOTE) (QUOTE INFXQUOTE) (QUOTE SPECOPER))


(DEFPROP FITSLINE 
 (LAMBDA(EXP COL PARS)
  (PROG (ANS EXPEXP EXPLGTH EXPLIM)
	(COND ((ATOM EXP) (RETURN T)))
	(SETQ EXPLGTH 0.)
	(SETQ EXPEXP EXP)
	(SETQ EXPLIM (DIFFERENCE (LINELENGTH NIL) (PLUS COL PARS)))
	(INITPROP (QUOTE INFXATOM) (QUOTE LGTHATOM) (QUOTE EXPR))
	(SETQ ANS (ERRSET (INFXEXPR EXPEXP 1. 0.)))
	(DELETEPROP (QUOTE INFXATOM) (QUOTE EXPR))
	(RETURN ANS))) 
EXPR)

(DEFPROP LGTHATOM 
 (LAMBDA(AT)
  (PROG NIL
	(SETQ EXPLGTH (PLUS EXPLGTH (FLATSIZE (GETINFXNAM AT))))
	(COND ((LEQ EXPLGTH EXPLIM) (RETURN NIL)))
	(SETQ EXPLGTH NIL)
	(ERR))) 
EXPR)

(DEFPROP TDD 
 (LAMBDA (EXP) (TDDEXP EXP 1. 0.)) 
EXPR)

(DEFPROP TDDARGS 
 (LAMBDA(ARGS COL PARS)
  (COND
   ((AND (NOT (NULL ARGS)) (NULL (CDR ARGS)))
    (PROG NIL
	  (PRINC (QUOTE / ))
	  (TDDEXP (CAR ARGS) (PLUS COL 1.) PARS)))
   (T
    (PROG NIL
	  (INFXATOM (QUOTE /())
	  (TDDLIST ARGS (PLUS COL 1.) (PLUS PARS 1.))
	  (INFXATOM (QUOTE /))))))) 
EXPR)

(DEFPROP TDDEXP 
 (LAMBDA(EXP COL PARS)
  (PROG (TEM)
	(TABTO COL)
	(COND
	 ((FITSLINE EXP COL PARS) (RETURN (INFXEXPR EXP 0. 0.))))
	(SETQ TEM (GETGET (CAR EXP) (QUOTE TDDFUN)))
	(COND
	 ((NOT (NULL TEM))
	  (RETURN (APPLY (PROPVAL TEM) (LIST EXP COL PARS)))))
   NOAT (TDDFUNC (CAR EXP) COL PARS)
	(TDDARGS (CDR EXP) (CURCOL) PARS))) 
EXPR)

(DEFPROP TDDFUNC 
 (LAMBDA(EXP COL PARS)
  (PROG NIL
	(COND ((ATOM EXP) (RETURN (INFXATOM EXP))))
	(INFXATOM (QUOTE /())
	(TDDEXP EXP (PLUS COL 1.) (PLUS PARS 1.))
	(INFXATOM (QUOTE /))))) 
EXPR)

(DEFPROP TDDLIST